Ja, herzlich willkommen.

Wir hatten nun kennengelernt eine semantische Behandlung der Aussagenlogik und eine beweistheoretische

Behandlung.

Nun sind wir Informatiker, wir wollen also eigentlich gerne Algorithmen haben, mit denen

wir mit Aussagenlogik umgehen.

Nun in der Tat kennen wir natürlich einen solchen Algorithmus bereits, das ist das Wahrheitstafelverfahren,

das wir schon kennengelernt haben.

Wenn wir also wissen wollen, ist zum Beispiel irgendeine Aussagenlogische Formel gültig,

dann stellen wir halt die Wahrheitstafel auf, gehen sie zeilenweise durch und überprüfen,

dass nun überall in jeder Zeile der Wahrheitstafel rechts ein Wahr steht und wenn das so ist,

dann sind wir glücklich, dass die Formel erfüllbar ist.

Das ist nun eine in jedem Falle nicht machbare Vorgehensweise für reale Anwendungen und

zwar deswegen, weil sie auf jeden Fall exponentiell lange dauert, in guten wie in schlechten Fällen.

Wir müssen immer die gesamte exponentiell lange Wahrheitstafel aufstellen, also wenn

wir n-propositionale Atome haben, hat die Wahrheitstafel zwei hoch n-Einträger, da

beißt die Maus keinen Faden ab und alle zwei hoch n-Einträger müssen wir überprüfen,

um herauszukriegen, dass eine Formel zum Beispiel eben erfüllbar oder gültig ist.

Gut, da wollen wir also ein effizienteres Verfahren kennenlernen, das also in der Praxis

auch tatsächlich Verwendung findet, also das Wahrheitstafelverfahren findet in der Praxis

tatsächlich keine Verwendung aus den gerade dargelegten Gründen und zwar ist das das

Resolutionsverfahren. So, das Resolutionsverfahren, das verlangt jetzt, dass Formeln in einer

bestimmten Normalform vorliegen, das heißt im ersten Teil der Sitzung befassen wir uns

mit Normalformen in der Aussagenlogik. Normalformen sind in der Logik insgesamt ein wichtiges

Thema und wir werden auch später in der Prädikatenlogik erster Stufe gewisse Normalformen kennenlernen.

Hier in der Aussagenlogik stellt sich das nun alles besonders glatt und einfach dar.

So und zwar werden diese Normalformen alle darauf hinauslaufen, dass wir verlangen, dass

wenn wir den Syntaxbaum einer Formel von oben her durchlaufen, dass dann die Konnektive,

die wir kennen, in einer bestimmten Reihenfolge auftreten. Wir werden jetzt also anfangen

jessermaßen in einer Formel die Konnektive so zu sortieren, dass immer eine Sorte am Anfang

auftritt, eine Sorte in der Mitte, eine am Schluss und wir fangen an mit der, die am

Schluss kommt, also am Schluss soll heißen, wenn ich im Syntaxbaum durchläufe bei den

Blättern und zwar soll das die Negation sein. Und das, der so entstehende Begriff von Normalform,

der hat eben eigene Bedeutung, deswegen hat er auch einen eigenen Namen, der heißt dann

Negations-Normalform, kurz NNF. So, die Negation soll ganz unten im Syntaxbaum

kommen, habe ich gesagt, sprich ganz innen. So, dazu müssen wir sie durch die anderen

Konnektive nach innen durchdrücken. Gut. Es ist sicher den meisten jetzt schon von

vornherein intuitiv klar, wie das also funktionieren wird. Wir haben ja diese demorgens schon Gesetze,

die uns gestatten, Negation praktisch mit sowohl Konjunktion als auch Dysjunktion zu

vertauschen. So, nun haben wir, wie man sich entsinnt, zum Beispiel Dysjunktion durch

Negation und Konjunktion ja überhaupt erst definiert. Das heißt, solange in dem Sinne

irgendwo Dysjunktionen in der Formel herumstehen, wird das also wohl nicht klappen mit Negationen

ganz nach innen schieben, weil sie ja versteckt in den Dysjunktionen immer noch dastehen.

Das heißt, da stellen wir uns also plötzlich jetzt für Zwecke der Negations-Normalform

auf einen ganz anderen Standpunkt. Wir sagen also jetzt. Ab jetzt, also für Zwecke unserer

Normalform-Betrachtung, sehen wir Dysjunktion als ein Basiskonnektiv an, also als Teil der

Grammatik. Und das machen wir auch gleich explizit in der neuen Grammatik für Negations-Normalform

klar, die wir jetzt hinschreiben. Also ich kann einfach Negations-Normalform definieren

durch eine Grammatik ähnlich der, mit der ich bereits die Aussagen logischen Formeln

insgesamt definiert habe. Sieht eben nur ein bisschen anders aus. Ja, noch etwas genauer.

Ich werde nicht nur Dysjunktionen, sondern auch die Konstant-Ware-Formel, die ja bisher